Nuprl Lemma : d-es_wf
11,40
postcript
pdf
D
:dsys{i:l},
E
:ES{i}. d-es{i:l}(
D
;
E
)
{i''}
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
,
es
is an event system of
D
,
x
:
A
.
B
(
x
)
,
P
&
Q
Lemmas
world
wf
,
fair-fifo
wf
,
possible-world
wf
,
event
system
wf
,
w-es
wf
,
dsys
wf
origin
D:dsys{i:l}, E:ES{i}. d-es{i:l}(D; E) 
{i''} D:dsys{i:l}, E:ES{i}. d-es{i:l}(D; E) {i''} x:A. B(x) T
x:A. B(x)